Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

Q is empty.


↳ QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, a), b), c), d) → F(a, b)
F(f(f(f(j, a), b), c), d) → F(f(a, b), f(f(a, d), c))
F(f(f(f(j, a), b), c), d) → F(a, d)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, a), b), c), d) → F(a, b)
F(f(f(f(j, a), b), c), d) → F(f(a, b), f(f(a, d), c))
F(f(f(f(j, a), b), c), d) → F(a, d)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule F(f(f(f(j, a), b), c), d) → F(f(a, b), f(f(a, d), c)) at position [] we obtained the following new rules:

F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(f(f(j, x0), x1), x2), y3), y2))
F(f(f(f(j, f(f(f(j, x0), x1), x2)), y1), y2), x3) → F(f(f(f(f(j, x0), x1), x2), y1), f(f(f(x0, x1), f(f(x0, x3), x2)), y2))
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(f(f(j, x0), x1), x2), y3), y2))
F(f(f(f(j, f(f(f(j, x0), x1), x2)), y1), y2), x3) → F(f(f(f(f(j, x0), x1), x2), y1), f(f(f(x0, x1), f(f(x0, x3), x2)), y2))
F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, a), b), c), d) → F(a, b)
F(f(f(f(j, a), b), c), d) → F(a, d)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(f(f(j, x0), x1), x2), y3), y2)) at position [1,0] we obtained the following new rules:

F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, f(f(f(j, x0), x1), x2)), y1), y2), x3) → F(f(f(f(f(j, x0), x1), x2), y1), f(f(f(x0, x1), f(f(x0, x3), x2)), y2))
F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, a), b), c), d) → F(a, b)
F(f(f(f(j, a), b), c), d) → F(a, d)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule F(f(f(f(j, f(f(f(j, x0), x1), x2)), y1), y2), x3) → F(f(f(f(f(j, x0), x1), x2), y1), f(f(f(x0, x1), f(f(x0, x3), x2)), y2)) at position [0] we obtained the following new rules:

F(f(f(f(j, f(f(f(j, x0), x1), x2)), y1), y2), x3) → F(f(f(x0, x1), f(f(x0, y1), x2)), f(f(f(x0, x1), f(f(x0, x3), x2)), y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, a), b), c), d) → F(a, b)
F(f(f(f(j, a), b), c), d) → F(a, d)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule F(f(f(f(j, a), b), c), d) → F(a, b) we obtained the following new rules:

F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x1)
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x1)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x1)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ ForwardInstantiation
                        ↳ QDP
                          ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x1)
F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x1)
F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, a), b), c), d) → F(a, d)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x1)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule F(f(f(f(j, a), b), c), d) → F(a, d) we obtained the following new rules:

F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6), x3)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5), x3)
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x3)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ ForwardInstantiation
                        ↳ QDP
                          ↳ ForwardInstantiation
                            ↳ QDP
                              ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6), x3)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x1)
F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x1)
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x3)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x1)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

The set Q consists of the following terms:

f(f(f(f(j, x0), x1), x2), x3)

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ Narrowing
            ↳ QDP
              ↳ Rewriting
                ↳ QDP
                  ↳ Rewriting
                    ↳ QDP
                      ↳ ForwardInstantiation
                        ↳ QDP
                          ↳ ForwardInstantiation
                            ↳ QDP
                              ↳ MNOCProof
                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), y_5), y_6), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x1)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x3)
F(f(f(f(j, a), b), c), d) → F(f(a, d), c)
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x1)
F(f(f(f(j, f(f(f(j, x0), x1), x2)), x3), y2), y3) → F(f(f(x0, x1), f(f(x0, x3), x2)), f(f(f(x0, x1), f(f(x0, y3), x2)), y2))
F(f(f(f(j, f(f(j, x0), x1)), y1), x3), x2) → F(f(f(f(j, x0), x1), y1), f(f(x0, x1), f(f(x0, x3), x2)))
F(f(f(f(j, f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), y_4), y_5), x3)
F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), x1), x2), x3) → F(f(f(f(j, y_0), y_1), y_2), x3)
F(f(f(f(j, f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4)), x1), x2), x3) → F(f(f(f(j, f(f(f(j, y_0), y_1), y_2)), y_3), y_4), x3)
F(f(f(f(j, f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3)), x1), x2), x3) → F(f(f(f(j, f(f(j, y_0), y_1)), y_2), y_3), x1)

The TRS R consists of the following rules:

f(f(f(f(j, a), b), c), d) → f(f(a, b), f(f(a, d), c))

Q is empty.
We have to consider all (P,Q,R)-chains.